perm filename MTC71.QUA[ESS,JMC] blob
sn#005531 filedate 1971-11-03 generic text, type T, neo UTF8
00900
01000
01100
01200
01300
01400
01500
01600 STANFORD UNIVERSITY
01700
01800
01900 COMPUTER SCIENCE DEPARTMENT
02000
02100 October 30, 1971
02200
02300
02400
02500
02600
02700
02800
02900
03000 Ph.D. QUALIFYING EXAMINATION
03100
03200
03300 Mathematical Aspects of Computation
03400
03500
03600
03700
03800
03900
04000
04100
04200
04300
04400
04500 The examination is open book. The first session is from 9:30AM to
04600 12:30 PM, and the second session is from 1:30 PM to 4:30 PM. No work
04700 on the exam is to be done during the lunch break. Both sessions are
04800 in room Polya 111.
04900
05000 Do 5 of the 6 problems, each in a separate blue book.
00100 1. Consider the recursive schema P defined by
00200
00300 F(x) ← if p(x) then x else F(b(F(a(x)))) ,
00400
00500 where p is a unary predicate symbol and a and b are unary
00600 function symbols.
00700
00800 It is an open problem whether this recursive schema can be
00900 translated to an equivalent flowchart schema. However, it can be
01000 translated if we add extra features to our class of flowchart
01100 schemas, such as counters, pushdown stacks, equality tests (allowing
01200 tests of the equality of two terms), arrays, etc.
01300
01400 Discuss in detail the translation of the recursive schema P
01500 to three such flowchart schemas. Be clear!
00100 2. a. Define modified algorithms for resolution and unification,
00200 incorporating an associative law for a particular function f of two
00300 arguments. Concretely, the new law of resolution must be such that
00400 for any set S of clauses, {} ε R(S), i.e. the empty clause can be
00500 obtained from S by resolution, if and only if S is not
00600 satisfiable by any interpretation for which
00700
00800 (∀x,y,z)[f(f(x,y),z) = f(x,f(y,z))].
00900
01000 b. Sketch a proof that your algorithms achieve this goal.
00100 3. Ackermann's function F(x,y) is defined recursively over the
00200 natural numbers as follows:
00300
00400 F(x,y) ← if x=0 then y + 1
00500 else if y=0 then F(x-1,1)
00600 else F(x-1,F(x,y-1)).
00700
00800 The following is an "algol" program for computing F(M,N) for any
00900 pair of natural numbers M and N. The value of F(M,N) is obtained
01000 in A[1] where A is an infinitely long integer array.
01100
01200 a. Attach an appropriate inductive assertion at point α and
01300 show partial correctness of the program. Be brief!
01400
01500 b. Prove that the program terminates for any pair M and N
01600 of natural numbers. Be precise!
01700
01800
01900 start: A[1] ← M;
02000 A[2] ← N;
02100 I ← 2;
02200 α: if I = 1 then go to halt;
02300 if A[I-1] = 0 then begin A[I-1] ← A[I]+1; I ← I-1; go to α end;
02400 if A[I] = 0 then begin A[I-1] ← A[I-1]-1; A[I] ← 1; go to α end;
02500 A[I+1] ← A[I]-1;
02600 A[I] ← A[I-1];
02700 A[I-1] ← A[I-1]-1;
02800 I ← I+1;
02900 go to α;
03000 halt:
00100 4. Suppose that the function c(P) is an effective measure of the
00200 computational cost of a parameterless program P depending
00300 monotonically on the size and running time of P. We require that
00400 c(P) be defined if P terminates, but it need not be defined if P
00500 does not terminate. Give the weakest conditions you can on the
00600 function c, such that a program of least cost having given output
00700 can be effectively constructed. (Assume some fixed definite machine
00800 by which programs are executed.
00100 5. A lion and a Christian are released at points a and b
00200 respectively in an arena and move alternately the Christian first. If
00300 it is the Christian's turn and she is at point x, she can go to her
00400 choice of points c1(x), c2(x), and c3(x). If it is the lion's
00500 turn and it is at point x, it has a choice of l1(x), l2(x), and
00600 l3(x).
00700
00800 Let E be a sentence of first order logic that axiomatizes
00900 whatever properties we wish to specify of a, b, the c's and the
01000 l's.
01100
01200 Strategies for the Christian and the lion may be specified by
01300 giving predicates pc1(x,y), pc2(x,y), pl1(x,y), and pl2(x,y) that
01400 give the conditions for the Christian or lion to make move 1 or 2
01500 when the Christian and lion are at positions x and y respectively.
01600
01700 If the positions of the Christian and lion are ever the same,
01800 the chase terminates with the lion eating the Christian.
03000
03100 Let F be a sentence of first order logic that axiomatizes
03200 whatever properties we wish to specify about the predicates pc1,
03300 pc2, pl1, and pl2. (It may include a, b, and the c's and l's.)
03400
03500 a. Write a sentence of first order logic that is provable if
03600 and only if the lion will catch the Christian in all interpretations
03700 of the constants predicates, and functions satisfying E and F.
03800
03900 b. Write a sentence of first order logic that is provable if
04000 and only if there is a strategy for the lion that will catch the
04100 Christian independently of what the Christian does in all
04200 interpretations of the constants, predicates, and functions
04300 satisfying E.
00100 6. Let PC stand for first order predicate calculus without equality,
00200 and let PCE stand for first order predicate calculus with equality.
00300 In PCE are allowed atomic formulas of the form t=u where t and
00400 u are any terms.
00500
00600 Herbrand's theorem for PC can be stated as follows: A set
00700 S of clauses is unsatisfiable if and only if there is a finite
00800 unsatisfiable set S' of ground instances of clauses of S.
00900
01000 a. Prove Herbrand's theorem for PC. Be brief!
01100
01200 b. Give a counterexample to show that the theorem does not hold for
01300 PCE.
01400
01500 c. Suggest a modified Herbrand's theorem for PCE and prove it. Be
01600 brief!
01700
01800
01900 REMEMBER TO DO ONLY 5 PROBLEMS EACH IN A SEPARATE BLUE BOOK!!!